\begin{tabbing}
f2f+{-}event\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it ff}$; ${\it f2f+}$; ${\it sndr}$; ${\it rcvr}$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=snd{-}it(${\it ff}$;f2f+Req(${\it f2f+}$);$e$;${\it sndr}$;${\it rcvr}$)\+
\\[0ex]$\vee$ rcv{-}it(${\it ff}$;f2f+Ack(${\it f2f+}$);$e$;${\it sndr}$;${\it rcvr}$)
\\[0ex]$\vee$ snd{-}it(${\it ff}$;f2f+Ack(${\it f2f+}$);$e$;${\it rcvr}$;${\it sndr}$)
\\[0ex]$\vee$ rcv{-}it(${\it ff}$;f2f+Req(${\it f2f+}$);$e$;${\it rcvr}$;${\it sndr}$)
\-
\end{tabbing}